ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;Top + A).
interface-right(X)  Interface(ds;da;A) 

latex

Definitions	Top, t  T, left + right, f(a), x:AB(x), x:A. B(x), invert-union(x), x.A(x), f o g  , let i,k:LocKnd = ik in P(i;k), x:A  B(x), {x:A| B(x)} , LocKnd, Type, Id, Knd, hasloc(k;i), b, x,y. t(x;y), (x  l), type List, let x,y = A in B(x;y), a:A fp B(a), x:A.B(x), x. t(x), g o f, interface-right(X), Interface(ds;da;A)
Lemmas	fpf-compose wf, l member wf, LocKnd wf, locknd-spread wf2, assert wf, hasloc wf, Knd wf, Id wf, p-compose wf, invert-union wf, top wf